(* -*-sml-*- *)
(*****************************************************************************)
(* Sanity checking "ExecuteSemantics": a derived executable semantics        *)
(* Not for compiling.                                                        *)
(*****************************************************************************)

val _ = loadPath := "../official-semantics" :: 
                    "../regexp"             :: 
                    !loadPath;

val _ = app load ["bossLib","intLib","regexpLib","ExecuteTools"];

val _ = quietdec := true;
open bossLib regexpLib;
val _ = quietdec := false;

fun pth t = let val () = print ("\n" ^ thm_to_string t ^ "\n\n") in t end;
val EVAL = pth o bossLib.EVAL;
val Define = pth o bossLib.Define;

(******************************************************************************
* Set the trace level of the regular expression library:
* 0: silent
* 1: 1 character (either - or +) for each list element processed
* 2: matches as they are discovered
* 3: transitions as they are calculated
* 4: internal state of the automata
******************************************************************************)
val _ = set_trace "regexpTools" 2;

(******************************************************************************
* Set default parsing to natural numbers rather than integers
******************************************************************************)
val _ = intLib.deprecate_int();

(******************************************************************************
* Examples
******************************************************************************)

(******************************************************************************
* [{s0};{s1};{s2}]  |=  [f1 U f2]   (f1, f2 arbitrary formulas)
******************************************************************************)
val _ = EVAL ``UF_SEM (FINITE[s0;s1;s2]) (F_UNTIL(f1,f2))``;

(******************************************************************************
* [{s0};{s1};{s2}]  |=  [b1 U b2]   (b1, b2 arbitrary boolean expressions )
******************************************************************************)
val _ = EVAL ``UF_SEM (FINITE[s0;s1;s2]) (F_UNTIL(F_BOOL b1, F_BOOL b2))``;

(******************************************************************************
* [{s0};{s1};{s2}]  |=  [p1 U p2]   (p1, p2 arbitrary atomic propositions)
******************************************************************************)
val _ =
EVAL
 ``UF_SEM (FINITE[s0;s1;s2]) (F_UNTIL(F_BOOL(B_PROP p1), F_BOOL(B_PROP p2)))``;

(******************************************************************************
* [{s0};{s1};{s2}]  |=  {1}(2)
******************************************************************************)
val _ =
EVAL
 ``UF_SEM (FINITE[s0;s1;s2]) (F_UNTIL(F_BOOL(B_PROP 1), F_BOOL(B_PROP 2)))``;

(******************************************************************************
* [{1};{1};{2}]  |=  {1}(2)
******************************************************************************)
val _ =
EVAL
 ``UF_SEM (FINITE[{1};{1};{2}]) (F_UNTIL(F_BOOL(B_PROP 1), F_BOOL(B_PROP 2)))``;

(******************************************************************************
* [{1};{3};{2}]  |=  {1}(2)
******************************************************************************)
val _ =
EVAL
 ``UF_SEM (FINITE[{1};{3};{2}]) (F_UNTIL(F_BOOL(B_PROP 1), F_BOOL(B_PROP 2)))``;

(* Can't evaluate a variable regular expression using automata!
EVAL ``UF_SEM (FINITE[s0;s1;s2]) (F_SUFFIX_IMP(r,f))``;
EVAL ``UF_SEM (FINITE[{1};{3};{2}]) (F_SUFFIX_IMP(r,f))``;
*)

(******************************************************************************
* [{1};{2};{3}]  |=  {n}(f)
******************************************************************************)
val _ =
EVAL
``UF_SEM (FINITE[{1};{2};{3}])
   (F_SUFFIX_IMP (S_BOOL (B_PROP n), f))``;

(******************************************************************************
* [{1};{2};{3}]  |=  {n}(p)
******************************************************************************)
val _ =
EVAL
``UF_SEM (FINITE[{1};{2};{3}])
   (F_SUFFIX_IMP (S_BOOL (B_PROP n), F_BOOL(B_PROP p)))``;

(******************************************************************************
* [{1};{2};{3}]  |=  {[*]}(f)
******************************************************************************)
val _ =
EVAL
``UF_SEM (FINITE[{1};{2};{3}])
   (F_SUFFIX_IMP (S_REPEAT S_TRUE, f))``;

(******************************************************************************
* [{1};{2};{3}]  |=  {[*]}(p)
******************************************************************************)
val _ =
EVAL
``UF_SEM (FINITE[{1};{2};{3}])
   (F_SUFFIX_IMP (S_REPEAT S_TRUE, F_BOOL(B_PROP p)))``;

(******************************************************************************
* [{p};{p};{p}]  |=  {[*]}(p)
******************************************************************************)
val _ =
EVAL
``UF_SEM (FINITE[{p};{p};{p}])
   (F_SUFFIX_IMP (S_REPEAT S_TRUE, F_BOOL(B_PROP p)))``;

(******************************************************************************
* [{p1};{p2};{p3}]  |=  {[*]}(p)
******************************************************************************)
val _ =
EVAL
``UF_SEM (FINITE[{p1};{p2};{p3}])
   (F_SUFFIX_IMP (S_REPEAT S_TRUE, F_BOOL(B_PROP p)))``;

(******************************************************************************
* [{1};{2};{3};{4};{5};{6};{7};{8};{9}]  |=  {3}(f)
******************************************************************************)
val _ =
EVAL
``UF_SEM (FINITE[{1};{2};{3};{4};{5};{6};{7};{8};{9}])
   (F_SUFFIX_IMP(S_BOOL(B_PROP 3), f))``;

(******************************************************************************
* [{1};{2};{3};{4};{5};{6};{7};{8};{9}]  |=  {[*];2;3}(f)
******************************************************************************)
val _ =
EVAL
``UF_SEM (FINITE[{1};{2};{3};{4};{5};{6};{7};{8};{9}])
   (F_SUFFIX_IMP
    (S_CAT(S_REPEAT S_TRUE, S_CAT(S_BOOL (B_PROP 2),S_BOOL (B_PROP 3))),
     f))``;

(******************************************************************************
* [{1};{2};{3};{4};{5};{6};{7};{8};{9}]  |=  {[*];2:3}(f)
******************************************************************************)
val _ =
EVAL
``UF_SEM (FINITE[{1};{2};{3};{4};{5};{6};{7};{8};{9}])
   (F_SUFFIX_IMP
    (S_CAT(S_REPEAT S_TRUE, S_FUSION(S_BOOL (B_PROP 2),S_BOOL (B_PROP 3))),
     f))``;

(******************************************************************************
* [{1};{2};{3};{4};{5};{6};{7};{8};{9}]  |=  {[*];2;3;[*]}(f)
******************************************************************************)
val _ =
EVAL
``UF_SEM (FINITE[{1};{2};{3};{4};{5};{6};{7};{8};{9}])
   (F_SUFFIX_IMP
    (S_CAT(S_REPEAT S_TRUE,
           S_CAT(S_CAT(S_BOOL (B_PROP 2),S_BOOL (B_PROP 3)),
                 S_REPEAT S_TRUE)),
     f))``;

(******************************************************************************
* [{1};{2};{3}]  |=  {[*];3}
******************************************************************************)
val _ =
EVAL ``US_SEM [{1};{2};{3}] (S_CAT(S_REPEAT S_TRUE, S_BOOL(B_PROP 3)))``;

(******************************************************************************
* [{1};{2};{3}]  |=  {[*];2}
******************************************************************************)
val _ =
EVAL ``US_SEM [{1};{2};{3}] (S_CAT(S_REPEAT S_TRUE, S_BOOL(B_PROP 2)))``;

(******************************************************************************
* [{1};{2};{3}]  |=  {[*];2;[*]}
******************************************************************************)
val _ =
EVAL ``US_SEM
        [{1};{2};{3};{4};{5}]
        (S_CAT(S_REPEAT S_TRUE, S_CAT(S_BOOL(B_PROP 2), S_REPEAT S_TRUE)))``;

(******************************************************************************
* [{1};{2};{3};{4};{5};{6};{7};{8};{9}]  |=  {1|3} |-> {[*];3}!
******************************************************************************)
val _ =
EVAL
``UF_SEM (FINITE[{1};{2};{3};{4};{5};{6};{7};{8};{9}])
   (F_STRONG_IMP ((S_OR (S_BOOL (B_PROP 1), S_BOOL (B_PROP 3))),
                  (S_CAT (S_REPEAT S_TRUE, S_BOOL (B_PROP 3)))))``;

(******************************************************************************
* [{1};{1};{1};{1};{1};{1};{1};{1};{1}]  |=  always{1}
******************************************************************************)
val _ =
EVAL
``UF_SEM (FINITE[{1};{1};{1};{1};{1};{1};{1};{1};{1}])
   (F_SERE_ALWAYS(S_BOOL(B_PROP 1)))``;

(******************************************************************************
* [{1};{1};{1};{1};{1};{1};{1};{1};{1}]  |=  always{1;1}
******************************************************************************)
val _ =
EVAL
``UF_SEM (FINITE[{1};{1};{1};{1};{1};{1};{1};{1};{1}])
   (F_SERE_ALWAYS(S_CAT(S_BOOL(B_PROP 1), S_BOOL(B_PROP 1))))``;

(******************************************************************************
* [{1};{2};{3};{4};{4;5};{4;6};{4;7};{4;8};{4;9}]  |=  always{4;4}
******************************************************************************)
val _ =
EVAL
``UF_SEM (FINITE[{1};{2};{3};{4};{4;5};{4;6};{4;7};{4;8};{4;9}])
   (F_SERE_ALWAYS(S_CAT(S_BOOL(B_PROP 4), S_BOOL(B_PROP 4))))``;

(******************************************************************************
* [{1};{2};{3};{4};{4};{6};{7};{8};{9}]  |=  never{4;3}
******************************************************************************)
val _ =
EVAL
``UF_SEM (FINITE[{1};{2};{3};{4};{4};{6};{7};{8};{9}])
   (F_SERE_NEVER(S_CAT(S_BOOL(B_PROP 4), S_BOOL(B_PROP 3))))``;

(******************************************************************************
* [{1};{2};{3};{4};{4};{6};{7};{8};{9}]  |=  never{3;4}
******************************************************************************)
val _ =
EVAL
``UF_SEM (FINITE[{1};{2};{3};{4};{4};{6};{7};{8};{9}])
   (F_SERE_NEVER(S_CAT(S_BOOL(B_PROP 3), S_BOOL(B_PROP 4))))``;


(******************************************************************************
quietdec:=true;;
loadPath := "../official-semantics" :: "../regexp" :: !loadPath;
app load ["res_quanTools","PropertiesTheory"];
open PSLPathTheory;
val resq_SS =
 simpLib.merge_ss
  [res_quanTools.resq_SS,
   rewrites
    [num_to_def,xnum_to_def,IN_DEF,num_to_def,xnum_to_def,LENGTH_def]];
quietdec:=false;

val UF_SEM_SUFFIX_IMP_FALSE =
 store_thm
  ("UF_SEM_SUFFIX_IMP_FALSE",
   ``UF_SEM w (F_SUFFIX_IMP(r, F_BOOL B_FALSE)) =
      !j::(0 to LENGTH w). ~(US_SEM (SEL w (0,j)) r)``,
   RW_TAC (std_ss++resq_SS) [UF_SEM_def,B_SEM]);
******************************************************************************)

(******************************************************************************
* Generated this from a Verilog model of the BUF example in
* Chapter 4 of FoCs User's Manual (see test.v)
* (www.haifa.il.ibm.com/projects/verification/focs/)
******************************************************************************)

(******************************************************************************
* String version
* val StoB_REQ = ``"StoB_REQ"``;
* val BtoS_ACK = ``"BtoS_ACK"``;
* val BtoR_REQ = ``"BtoR_REQ"``;
* val RtoB_ACK = ``"RtoB_ACK"``;
******************************************************************************)

(******************************************************************************
* Num version
******************************************************************************)
val StoB_REQ_def = Define `StoB_REQ = 0`;
val BtoS_ACK_def = Define `BtoS_ACK = 1`;
val BtoR_REQ_def = Define `BtoR_REQ = 2`;
val RtoB_ACK_def = Define `RtoB_ACK = 3`;

quietdec := true;
val SimRun_def =
 Define
  `SimRun =
      [{};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {}]`;

quietdec := false;

(* A pure computeLib version *)

(******************************************************************************
* SimRun |= {[*]; StoB_REQ; [*]}
******************************************************************************)
val _ =
time
 EVAL
 ``US_SEM
    SimRun
    (S_CAT(S_REPEAT S_TRUE,
           S_CAT(S_BOOL(B_PROP StoB_REQ),
                 S_REPEAT S_TRUE)))``;

(******************************************************************************
* SimRun |= {[*]; StoB_REQ; StoB_REQ; [*]}
******************************************************************************)
val _ =
time
 EVAL
 ``US_SEM
    SimRun
    (S_CAT(S_REPEAT S_TRUE,
           S_CAT(S_CAT(S_BOOL(B_PROP StoB_REQ),S_BOOL(B_PROP StoB_REQ)),
                 S_REPEAT S_TRUE)))``;


(******************************************************************************
* SimRun |= {[*]; StoB_REQ; BtoR_REQ; [*]}
******************************************************************************)
val _ =
time
 EVAL
 ``US_SEM
    SimRun
    (S_CAT(S_REPEAT S_TRUE,
           S_CAT(S_CAT(S_BOOL(B_PROP StoB_REQ),S_BOOL(B_PROP BtoR_REQ)),
                 S_REPEAT S_TRUE)))``;

(******************************************************************************
* The following 4 properties make up the vunit
* four_phase_handshake_left of page 19 of the FoCs User's Manual
* with "never r" replaced by "{r}(F)"
******************************************************************************)

(******************************************************************************
* {[*]; !StoB_REQ & BtoS_ACK; StoB_REQ}(F)
******************************************************************************)
val _ =
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
      (S_CAT(S_REPEAT S_TRUE,
             S_CAT(S_BOOL(B_AND(B_NOT(B_PROP StoB_REQ), B_PROP BtoS_ACK)),
                   S_BOOL(B_PROP StoB_REQ))),
       F_BOOL B_FALSE))``;

(******************************************************************************
* FINITE SimRun |= {[*]; StoB_REG & !BtoS_ACK; !StoB_REQ}(F)
******************************************************************************)
val _ =
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
      (S_CAT(S_REPEAT S_TRUE,
             S_CAT(S_BOOL(B_AND(B_PROP StoB_REQ, B_NOT(B_PROP BtoS_ACK))),
                   S_BOOL(B_NOT(B_PROP StoB_REQ)))),
       F_BOOL B_FALSE))``;

(******************************************************************************
* FINITE SimRun |= {[*]; !BtoS_ACK & !StoB_REQ; BtoS_ACK}(F)
******************************************************************************)
val _ =
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
      (S_CAT(S_REPEAT S_TRUE,
             S_CAT(S_BOOL(B_AND(B_NOT(B_PROP BtoS_ACK),
                                B_NOT(B_PROP StoB_REQ))),
                   S_BOOL(B_PROP BtoS_ACK))),
       F_BOOL B_FALSE))``;

(******************************************************************************
* {[*]; BtoS_ACK & StoB_REQ; !BtoS_ACK}(F)
******************************************************************************)
val _ =
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
      (S_CAT(S_REPEAT S_TRUE,
             S_CAT(S_BOOL(B_AND(B_PROP BtoS_ACK, B_PROP StoB_REQ)),
                   S_BOOL(B_NOT(B_PROP BtoS_ACK)))),
       F_BOOL B_FALSE))``;


(******************************************************************************
* Make "&" into an infix for F_AND
******************************************************************************)
val _ = set_fixity "&" (Infixl 500);
val F_AND_IX_def = xDefine "F_AND_IX" `$& f1 f2 = F_AND(f1,f2)`;

(******************************************************************************
* A single property characterising a four-phase handshake
******************************************************************************)

val FOUR_PHASE_def =
 Define
  `FOUR_PHASE req ack =
    F_SUFFIX_IMP
     (S_CAT(S_REPEAT S_TRUE,
            S_CAT(S_BOOL(B_AND(B_NOT(B_PROP req), B_PROP ack)),
                  S_BOOL(B_PROP req))),
      F_BOOL B_FALSE)
    &
    F_SUFFIX_IMP
     (S_CAT(S_REPEAT S_TRUE,
            S_CAT(S_BOOL(B_AND(B_PROP req, B_NOT(B_PROP ack))),
                  S_BOOL(B_NOT(B_PROP req)))),
      F_BOOL B_FALSE)
    &
    F_SUFFIX_IMP
     (S_CAT(S_REPEAT S_TRUE,
            S_CAT(S_BOOL(B_AND(B_NOT(B_PROP ack), B_NOT(B_PROP req))),
                  S_BOOL(B_PROP ack))),
      F_BOOL B_FALSE)
    &
    F_SUFFIX_IMP
     (S_CAT(S_REPEAT S_TRUE,
            S_CAT(S_BOOL(B_AND(B_PROP ack, B_PROP req)),
                  S_BOOL(B_NOT(B_PROP ack)))),
      F_BOOL B_FALSE)`;

(******************************************************************************
* vunit four_phase_handskake_left (page 19, FoCs User's Manual)
* FOUR_PHASE StoB_REQ BtoS_ACK
******************************************************************************)
val _ =
time EVAL ``UF_SEM (FINITE SimRun) (FOUR_PHASE StoB_REQ BtoS_ACK)``;


(******************************************************************************
* vunit four_phase_handskake_right (page 20, FoCs User's Manual)
* FOUR_PHASE BtoR_REQ RtoB_ACK
******************************************************************************)
val _ =
time EVAL ``UF_SEM (FINITE SimRun) (FOUR_PHASE BtoR_REQ RtoB_ACK)``;

(******************************************************************************
* f1 before f2 = [not f2 W (f1 & not f2)]
******************************************************************************)
val F_BEFORE_def =
 Define
  `F_BEFORE(f1,f2) = F_W(F_NOT f2, F_AND(f1, F_NOT f2))`;

(******************************************************************************
* FINITE SimRun |= StoB_REQ before BtoS_ACK
******************************************************************************)
val _ =
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_BEFORE(F_BOOL(B_PROP StoB_REQ), F_BOOL(B_PROP BtoS_ACK)))``;

(******************************************************************************
* FINITE SimRun |= BtoS_ACK before StoB_REQ
******************************************************************************)
val _ =
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_BEFORE(F_BOOL(B_PROP BtoS_ACK), F_BOOL(B_PROP StoB_REQ)))``;

(******************************************************************************
* FINITE SimRun |= {[*]}(StoB_REQ before BtoS_ACK)
******************************************************************************)
val _ =
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     (S_REPEAT S_TRUE,
      F_BEFORE(F_BOOL(B_PROP StoB_REQ), F_BOOL(B_PROP BtoS_ACK))))``;

(******************************************************************************
* FINITE SimRun |= {[*]}(BtoS_ACK before StoB_REQ)
******************************************************************************)
val _ =
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     (S_REPEAT S_TRUE,
      F_BEFORE(F_BOOL(B_PROP BtoS_ACK), F_BOOL(B_PROP StoB_REQ))))``;


(******************************************************************************
* Make ";;" into an infix for S_CAT
******************************************************************************)
val _ = set_fixity ";;" (Infixl 500);
val S_CAT_IX_def = xDefine "S_CAT_IX" `$;; r1 r2 = S_CAT(r1,r2)`;

(******************************************************************************
* FINITE SimRun |= {[*];!BtoS_ACK;BtoS_ACK}(F)
******************************************************************************)
val _ =
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;;
       S_BOOL(B_PROP BtoS_ACK)),
      F_BOOL B_FALSE))``;

(******************************************************************************
* FINITE SimRun |= {[*];!BtoS_ACK;BtoS_ACK;[*];!BtoS_ACK;BtoS_ACK}(F)
******************************************************************************)
val _ =
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;;
       S_BOOL(B_PROP BtoS_ACK) ;;
       S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;;
       S_BOOL(B_PROP BtoS_ACK)),
      F_BOOL B_FALSE))``;

(******************************************************************************
* FINITE SimRun |= {[*];BtoS_ACK;[RtoB_ACK];BtoS_ACK}(F)
******************************************************************************)
val _ =
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_PROP BtoS_ACK) ;;
       S_REPEAT(S_BOOL(B_PROP RtoB_ACK)) ;;
       S_BOOL(B_PROP BtoS_ACK)),
      F_BOOL B_FALSE))``;

(******************************************************************************
* FINITE SimRun |= {[*];!BtoS_ACK;BtoS_ACK;[RtoB_ACK];!BtoS_ACK;BtoS_ACK}(F)
******************************************************************************)
val _ =
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;;
       S_BOOL(B_PROP BtoS_ACK) ;;
       S_REPEAT(S_BOOL(B_PROP RtoB_ACK)) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;;
       S_BOOL(B_PROP BtoS_ACK)),
      F_BOOL B_FALSE))``;

(******************************************************************************
* FINITE SimRun |= {[*];BtoS_ACK;[!RtoB_ACK];BtoS_ACK}(F)
******************************************************************************)
val _ =
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_PROP BtoS_ACK) ;;
       S_REPEAT(S_BOOL(B_NOT(B_PROP RtoB_ACK))) ;;
       S_BOOL(B_PROP BtoS_ACK)),
      F_BOOL B_FALSE))``;

(******************************************************************************
* FINITE SimRun |= {[*];!BtoS_ACK;BtoS_ACK;[!RtoB_ACK];!BtoS_ACK;BtoS_ACK}(F)
******************************************************************************)
val _ =
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;;
       S_BOOL(B_PROP BtoS_ACK) ;;
       S_REPEAT(S_BOOL(B_NOT(B_PROP RtoB_ACK))) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;;
       S_BOOL(B_PROP BtoS_ACK)),
      F_BOOL B_FALSE))``;

(******************************************************************************
* FINITE SimRun
*  |= {[*];!BtoS_ACK;BtoS_ACK;[*];!RtoB_ACK;RtoB_ACK;[*];!BtoS_ACK;BtoS_ACK}(F)
******************************************************************************)
val _ =
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;;
       S_BOOL(B_PROP BtoS_ACK) ;;
       S_REPEAT(S_BOOL(B_TRUE)) ;;
       S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;;
       S_BOOL(B_PROP RtoB_ACK) ;;
       S_REPEAT(S_BOOL(B_TRUE)) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;;
       S_BOOL(B_PROP BtoS_ACK)),
      F_BOOL B_FALSE))``;

(******************************************************************************
* SimRun
*  |= {[*];!BtoS_ACK;BtoS_ACK;
*          [BtoS_ACK];[!BtoS_ACK];
*          ((!RtoB_ACK;RtoB_ACK;)&&(!BtoS_ACK;!BtoS_ACK));
*          [!BtoS_ACK];BtoS_ACK}
******************************************************************************)
val _ =
time
 EVAL
 ``US_SEM
    SimRun
      ((S_REPEAT(S_BOOL B_TRUE) ;;
        S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;;
        S_BOOL(B_PROP BtoS_ACK) ;;
        S_REPEAT(S_BOOL(B_PROP BtoS_ACK));;
        S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));;
        S_AND((S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;; S_BOOL(B_PROP RtoB_ACK)),
              (S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)))) ;;
        S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));;
        S_BOOL(B_PROP BtoS_ACK)))``;

(******************************************************************************
* FINITE SimRun
*  |= {[*];!BtoS_ACK;BtoS_ACK;
*          [BtoS_ACK];[!BtoS_ACK];
*          ((!RtoB_ACK;RtoB_ACK;)&&(!BtoS_ACK;!BtoS_ACK));
*          [!BtoS_ACK];BtoS_ACK}
*     (F)
******************************************************************************)
val _ =
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;;
       S_BOOL(B_PROP BtoS_ACK) ;;
       S_REPEAT(S_BOOL(B_PROP BtoS_ACK));;
       S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));;
       S_AND((S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;; S_BOOL(B_PROP RtoB_ACK)),
             (S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)))) ;;
       S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));;
       S_BOOL(B_PROP BtoS_ACK)),
      F_BOOL B_FALSE))``;

(******************************************************************************
* FINITE SimRun
*  |= {[*];!BtoS_ACK;BtoS_ACK;
*          [BtoS_ACK];[!BtoS_ACK];
*          ((!RtoB_ACK;RtoB_ACK;)&&(!BtoS_ACK;!BtoS_ACK));
*          [!BtoS_ACK];BtoS_ACK}
*     (T)
******************************************************************************)
val _ =
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;;
       S_BOOL(B_PROP BtoS_ACK) ;;
       S_REPEAT(S_BOOL(B_PROP BtoS_ACK));;
       S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));;
       S_AND((S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;; S_BOOL(B_PROP RtoB_ACK)),
             (S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)))) ;;
       S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));;
       S_BOOL(B_PROP BtoS_ACK)),
      F_BOOL B_TRUE))``;
(******************************************************************************
* FINITE SimRun
*  |= {[*];!BtoS_ACK;
*          BtoS_ACK;
*          [BtoS_ACK&!RtoB_ACK];
*          [!BtoS_ACK&!RoB_ACK];
*          BtoS_ACK}
*     (F)
******************************************************************************)
val _ =
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;;
       S_BOOL(B_PROP BtoS_ACK) ;;
       S_REPEAT(S_BOOL(B_AND(B_PROP BtoS_ACK,
                             B_NOT(B_PROP RtoB_ACK)))) ;;
       S_REPEAT(S_BOOL(B_AND(B_NOT(B_PROP BtoS_ACK),
                             B_NOT(B_PROP RtoB_ACK)))) ;;
       S_BOOL(B_PROP BtoS_ACK)),
      F_BOOL B_FALSE))``;


(******************************************************************************
* FINITE SimRun |= (!BtoS_ACK & X BtoS_ACK) before (!RtoB_ACK & X RtoB_ACK)
******************************************************************************)
val _ =
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_BEFORE
       (F_AND(F_NOT(F_BOOL(B_PROP RtoB_ACK)),
              F_NEXT(F_BOOL(B_PROP RtoB_ACK))),
        F_AND(F_NOT(F_BOOL(B_PROP BtoS_ACK)),
              F_NEXT(F_BOOL(B_PROP BtoS_ACK)))))``;

(******************************************************************************
* FINITE SimRun
*  |= {[*]; !BtoS_ACK; BtoS_ACK; true}
*     ((!RtoB_ACK & X RtoB_ACK) before (!BtoS_ACK & X BtoS_ACK))
******************************************************************************)
val _ =
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;;
       S_BOOL(B_PROP BtoS_ACK) ;;
       S_BOOL B_TRUE),
      F_BEFORE
       (F_AND(F_NOT(F_BOOL(B_PROP RtoB_ACK)),
              F_NEXT(F_BOOL(B_PROP RtoB_ACK))),
        F_AND(F_NOT(F_BOOL(B_PROP BtoS_ACK)),
              F_NEXT(F_BOOL(B_PROP BtoS_ACK))))))``;

(******************************************************************************
* FINITE SimRun
*  |= {[*]; !RtoB_ACK; RtoB_ACK; true}
*     ((!BtoS_ACK & X BtoS_ACK) before (!RtoB_ACK & X RtoB_ACK))
******************************************************************************)
val _ =
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;;
       S_BOOL(B_PROP RtoB_ACK) ;;
       S_BOOL B_TRUE),
      F_BEFORE
       (F_AND(F_NOT(F_BOOL(B_PROP BtoS_ACK)),
              F_NEXT(F_BOOL(B_PROP BtoS_ACK))),
        F_AND(F_NOT(F_BOOL(B_PROP RtoB_ACK)),
              F_NEXT(F_BOOL(B_PROP RtoB_ACK))))))``;


(******************************************************************************
* FINITE SimRun
*  |= {[*]; !BtoS_ACK; BtoS_ACK}
*     ((!RtoB_ACK & X RtoB_ACK) before (!BtoS_ACK & X BtoS_ACK))
******************************************************************************)
val _ =
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;;
       S_BOOL(B_PROP BtoS_ACK)),
      F_BEFORE
       (F_AND(F_NOT(F_BOOL(B_PROP RtoB_ACK)),
              F_NEXT(F_BOOL(B_PROP RtoB_ACK))),
        F_AND(F_NOT(F_BOOL(B_PROP BtoS_ACK)),
              F_NEXT(F_BOOL(B_PROP BtoS_ACK))))))``;

(******************************************************************************
* FINITE SimRun
*  |= {[*]; !RtoB_ACK; RtoB_ACK}
*     ((!BtoS_ACK & X BtoS_ACK) before (!RtoB_ACK & X RtoB_ACK))
******************************************************************************)
val _ =
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;;
       S_BOOL(B_PROP RtoB_ACK)),
      F_BEFORE
       (F_AND(F_NOT(F_BOOL(B_PROP BtoS_ACK)),
              F_NEXT(F_BOOL(B_PROP BtoS_ACK))),
        F_AND(F_NOT(F_BOOL(B_PROP RtoB_ACK)),
              F_NEXT(F_BOOL(B_PROP RtoB_ACK))))))``;

(******************************************************************************
* Generating checkers from formulas.
* An example from the Accellera PSL reference manual, page 45.
* Mentioned in Joe Hurd's ARG Lunch, 4 November 2003.
******************************************************************************)
val pureDefine = with_flag (computeLib.auto_import_definitions, false) Define;
val a_def = pureDefine `a = 0`;
val b_def = pureDefine `b = 1`;
val c_def = pureDefine `c = 2`;
val alpha = map Term [`a`,`b`,`c`];
val prop = ``F_AND (F_BOOL (B_PROP c),
               F_NEXT (F_W (F_BOOL (B_PROP a), F_BOOL (B_PROP b))))``;
val prop_sere = time EVAL ``checker ^prop``;
val sere = rhs (concl prop_sere);
val sere_re = time EVAL ``sere2regexp ^sere``;
val re = rhs (concl sere_re);
val dfa = verilog_dfa {alphabet = alpha, name = "Checker1", regexp = re};
val _ = print ("\n\n" ^ dfa ^ "\n\n");
